Fix rollback-handling in consistency trace validation - #8133
Merged
Amaury Chamayou (achamayou) merged 9 commits intoAug 19, 2026
Merged
Conversation
When a new primary reuses a sequence number after rollback, copying the entire prior ledger branch retains the invalid suffix and prevents the logged transaction from matching. Copy only the source prefix before the next implementation sequence number, bounded by the source branch length. Add a deterministic rollback trace that commits 2.10, invalidates 2.11, and reuses sequence 11 in view 3, and run it in continuous verification. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>
Document in the CI workflow why rollback coverage uses a hard-coded trace rather than a partitions test. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>
Cover elections without rollback, rollback of two transactions, and a non-contiguous view jump from 2 to 5. Run every checked-in consistency trace through the adapter in continuous verification. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>
Copilot started reviewing on behalf of
Amaury Chamayou (achamayou)
August 8, 2026 13:18
View session
Contributor
There was a problem hiding this comment.
Pull request overview
This PR updates the TLA+ consistency trace validator to correctly handle elections that roll back an uncommitted suffix and potentially reuse sequence numbers in a new view, preventing valid implementation traces from being incorrectly rejected.
Changes:
- Fix
BackfillLedgerBranchesto copy only the committed/known-safe prefix into newly created view branches (bounded by the next logged seqno and source length). - Add several deterministic NDJSON traces covering rollback, no-rollback elections, and non-contiguous view jumps.
- Extend CI to validate all checked-in consistency election traces via TLC trace validation (
tv) with a single worker.
Custom instructions used:
.github/copilot-instructions.md
Reviewed changes
Copilot reviewed 6 out of 6 changed files in this pull request and generated no comments.
Show a summary per file
| File | Description |
|---|---|
tla/consistency/TraceMultiNodeReads.tla |
Adjusts branch backfilling logic to avoid copying rolled-back suffix entries into new-view branches. |
tla/consistency/traces/rollback_two_transactions.ndjson |
Adds a trace where an uncommitted suffix is rolled back and seqnos are reused in a new view. |
tla/consistency/traces/rollback_same_seqno.ndjson |
Adds a trace explicitly reusing the same seqno after invalidation/rollback across views. |
tla/consistency/traces/election_non_contiguous_view.ndjson |
Adds a trace that jumps across views (e.g., 2 -> 5) to exercise repeated bounded copying. |
tla/consistency/traces/election_no_rollback.ndjson |
Adds a control trace where the full prior branch remains valid across an election (no rollback). |
.github/workflows/ci-verification.yml |
Validates all checked-in consistency traces in CI using single-worker TLC trace validation. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Heidi Howard (heidihoward)
approved these changes
Aug 19, 2026
Heidi Howard (heidihoward)
left a comment
Heidi Howard (heidihoward)
left a comment
Member
There was a problem hiding this comment.
Looks fine to me. Obviously we want to remove these hardcoded traces for proper trace checking when we are able
Amaury Chamayou (achamayou)
enabled auto-merge (squash)
August 19, 2026 12:50
Member
Author
Agreed, a larger change to the consistency trace validation is coming in the Lean PR. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Before the fix, whenever the trace referenced a view that the model had not created yet,
BackfillLedgerBranchescreated that view by copying the entire previous ledger branch. That assumes every entry from the previous primary survives an election. In reality, only the committed prefix is guaranteed to survive: an uncommitted suffix may be rolled back, and its sequence numbers may then be reused by the new primary.For example, suppose transaction A commits at
2.10, transaction B executes at2.11but is later invalidated, and transaction C executes at3.11. The old adapter copied B into the reconstructed view-3 branch, making that branch already 11 entries long. The validator requires the branch to contain exactly 10 entries before executing C at sequence 11, and its normal backfill actions can only append entries, not remove the stale suffix. Validation therefore dead-ended and reportedTraceMatchedas violated, incorrectly rejecting a valid implementation trace.The fix copies only the source prefix strictly before the next logged sequence number, bounded by the source branch length. This preserves the full branch when an election has no rollback, drops any rolled-back suffix when sequence numbers are reused, and lets the existing per-branch backfill add unknown non-client entries when the source is shorter than required. Applying the same bounded copy repeatedly also handles non-contiguous view jumps, such as moving directly from view 2 to view 5.